\begin{tabbing}
$\forall$$p$:FinProbSpace, $f$:($\mathbb{N}\rightarrow\mathbb{N}$), $X$:($n$:$\mathbb{N}\rightarrow$RandomVariable($p$;$f$($n$))), $s$, $k$:$\mathbb{Q}$.
\\[0ex]($\forall$$n$:$\mathbb{N}$, $i$:\{0..$n$$^{-}$\}. $f$($i$) $<$ $f$($n$))
\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}$.\+
\\[0ex]E($f$($n$);$X$($n$)) = 0 $\in$ $\mathbb{Q}$
\\[0ex]\& E($f$($n$);($x$.$x$ $\ast$ $x$) o $X$($n$)) = $s$
\\[0ex]\& E($f$($n$);($x$.($x$ $\ast$ $x$) $\ast$ $x$ $\ast$ $x$) o $X$($n$)) = $k$)
\-\\[0ex]$\Rightarrow$ ($\forall$$n$:$\mathbb{N}$, $i$:\{0..$n$$^{-}$\}. rv{-}disjoint($p$;$f$($n$);$X$($i$);$X$($n$)))
\\[0ex]$\Rightarrow$ ($\exists$\=$B$:$\mathbb{Q}$\+
\\[0ex](0 $\leq$ $B$ \& ($\forall$$n$:$\mathbb{N}$. E($f$($n$);($x$.($x$ $\ast$ $x$) $\ast$ $x$ $\ast$ $x$) o rv{-}partial{-}sum($n$;$i$.$X$($i$))) $\leq$ $B$ $\ast$ $n$ $\ast$ $n$)))
\-
\end{tabbing}